A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A). f   = f 

latex

Definitions	x.A(x), <a,b>, (x  l), {x:A| B(x) }, f(a), x(s), x:AB(x), s = t, Void, t  T, x:A. B(x), Top, type List, x:A. B(x), S  T, nil, as @ bs, f(x), x  dom(f), f(x)?z, f  g, , a:A fp B(a), x:AB(x), Type, x. t(x), EqDecider(T), False, P  Q, A, b, Prop, b, , deq-member(eq;x;L), P & Q, P  Q, Unit, left+right, , if b t else f fi
Lemmas	ifthenelse wf, it wf, unit wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, deq wf, fpf wf, l member wf, append-nil, top wf